Reference made herein and listed at the end are incorporated herein as necessary for understanding and implementing of the present disclosure.
Fixed-point saturating arithmetic is used widely in media and digital signal processing applications. Given a B-bit two's complement operation OP, its saturating counterpart detects overflow and sets the result to the limits of the representable number range:
                                          OP            sat                    ⁡                      (                          x              ,              y                        )                          =                                                            MaxB                ⁢                                                                  ⁢                if                ⁢                                                                  ⁢                                  OP                  ⁡                                      (                                          x                      ,                      y                                        )                                                  ⁢                                                                  ⁢                overflows                                                                                                                              MinB                    ⁢                                                                                  ⁢                    if                    ⁢                                                                                  ⁢                    OP                                    }                                ⁢                                  (                                      x                    ,                    y                                    )                                ⁢                                                                  ⁢                underflows                                                                                                          OP                  ⁡                                      (                                          x                      ,                      y                                        )                                                  ⁢                                                                  ⁢                otherwise                                                                        (        1        )            
For example, speech codecs in the GSM standard are expressed in terms of saturating arithmetic operations (Refs 1 and 2). A number of modern processor architectures, such as TI C6x, Intel IA-32 and ARM implement saturating arithmetic instructions.
Standard programming languages, such as ANSI C, do not provide operators for saturating arithmetic. Typically, application developers include libraries of functions or macros that implement these operations in terms of basic two's complement arithmetic. In order to obtain high performance on a given architecture, these libraries have to be coded either in assembly or using vendor-specific libraries or language extensions. This clearly complicates software development and maintenance. Various language extensions and standards have been proposed (Ref. 3). Their future is unclear, given the usual reluctance of established vendors to standardize. Thus, programmers are forced into the trade-off between portability and efficiency.
The way to resolve this trade-off is for a compiler to automatically recognize code fragments that implement saturating arithmetic and convert them into appropriate machine instructions. For this solution to be effective, the recognition algorithm must be robust and work across different coding styles. One can start with simple pattern matching on abstract syntax trees.
However, the limitations of such approach become evident as one consider various implementations of saturating addition. Examples are show in U.S. patent application Ser. No. 10/382,578. In order to prove, two saturated addition instructions are both equivalent to the definition in equation 1, one needs to prove equivalence between the results of the sequences of various bit manipulation and logical operations. Instead of an ad-hoc approach, a method that has a formal algebraic foundation is needed.
In the U.S. patent application Ser. No. 10/382,578, a method is described for recognition of saturated addition and subtraction specifically. The present disclosure recognizes that the principles in the previous application are applicable to any acyclic operation and may be expressed in generic terms.
The method of the present disclosure determines by an optimizing compiler whether any variable in the given program equals to the given acyclic mathematical function f(x,y, . . . ) applied to the given variables x, y, . . . in the program. In one embodiment, the method includes expressing the bits of the value of the function f(x,y, . . . ) as a Boolean function of the bits of the inputs x, y, . . . ; expressing, for every variable v and program statement s, the value taken by v when s is executed as a Boolean function V(s,v)(x, y, . . . ) of the bits of x, y, . . . ; and expressing, for every statement s, the condition under which the statement is executed as a Boolean function C(s)(x, y, . . . ) of the bits of the inputs x, y, . . . . Finally, a determination is made using a Boolean satisfiability oracle of whether, for the given variable v and program statement s, the following Boolean expression holds: C(s)(x,y, . . . )=>V(s,v)(x,y . . . )=f(x,y, . . . ).
In a second embodiment, the method includes expressing the value of f(x,y, . . . ) as a plurality of functions fj(x,y, . . . ) having the corresponding predicate Pj(x,y, . . . ); expressing, for every variable v and program statement s, the value taken by v when s is executed as a plurality of functions Vj(s,v)(x,y, . . . ), one for each predicate Pj(x,y, . . . ); and expressing, for every statement s, the condition under which the statement is executed as a plurality of functions Cj(s)(x,y, . . . ), one for each predicate Pj(x,y, . . . ). Finally, a determination is of whether for the given variable v and program statement s, Vj(s,v)(x,y, . . . )=fj(x,y, . . . ) whenever the predicate Pj(x,y, . . . ) and the condition Cj(s)(x,y, . . . ) are true.
In either embodiment, the program may be transformed so that the value of each variable v that takes on the value of the function f(x,y, . . . ) is computed by the available function f(x,y, . . . ) by adding the invocation of the instruction t=f(x,y, . . . ); and replacing each reference to variable v at each statement s, such that the value of v at s equals f(x,y, . . . ), with the reference to t. The instructions that are unused after the program transformation are eliminated by dead-code elimination. Where the mathematical function f(x, y, . . . ) is computable in hardware, the program may be transformed so that the value of each variable v that takes on the value of the function f(x,y, . . . ) is computed by the available hardware instruction for f(x,y, . . . ).
These and other aspects of the present invention will become apparent from the following detailed description of the invention, when considered in conjunction with accompanying drawings.